 /*
 * Main.java
 * 
 * Copyright 2004 Christoph Csallner and Yannis Smaragdakis.
 */
package edu.gatech.cc.cnc;

import static edu.gatech.cc.jcrasher.Assertions.check;
import static edu.gatech.cc.jcrasher.Assertions.notNull;

import java.lang.reflect.Array;
import java.lang.reflect.Constructor;
import java.lang.reflect.Member;
import java.lang.reflect.Method;
import java.util.Arrays;
import java.util.Hashtable;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Vector;

import java_cup.runtime.lr_parser;
import javafe.ast.ArrayType;
import javafe.ast.ConstructorDecl;
import javafe.ast.Expr;
import javafe.ast.FieldDecl;
import javafe.ast.GenericVarDecl;
import javafe.ast.Modifiers;
import javafe.ast.RoutineDecl;
import javafe.ast.Type;
import javafe.tc.TypeSig;
import javafe.util.Location;
import javafe.util.LocationManagerCorrelatedReader;
import edu.gatech.cc.cnc.params.JCrasherPlanner;
import edu.gatech.cc.cnc.params.Param;
import edu.gatech.cc.cnc.params.ParamArray;
import edu.gatech.cc.cnc.params.ParamComplex;
import edu.gatech.cc.cnc.params.ParamInt;
import edu.gatech.cc.cnc.params.ParamIntegral;
import edu.gatech.cc.cnc.params.ParamRefType;
import edu.gatech.cc.cnc.plans.stmt.BlockStatementSequence;
import edu.gatech.cc.cnc.plans.stmt.ConstructorCallingBlockStatementSequence;
import edu.gatech.cc.cnc.plans.stmt.MethodCallingBlockStatementSequence;
import edu.gatech.cc.jcrasher.JCrasher;
import edu.gatech.cc.jcrasher.Constants.Visibility;
import edu.gatech.cc.jcrasher.plans.JavaCode;
import edu.gatech.cc.jcrasher.plans.expr.Expression;
import edu.gatech.cc.jcrasher.plans.stmt.Block;
import edu.gatech.cc.jcrasher.plans.stmt.BlockStatement;
import edu.gatech.cc.jcrasher.types.TypeGraph;
import edu.gatech.cc.jcrasher.types.TypeGraphImpl;
import edu.gatech.cc.jcrasher.writer.JUnitAll;
import edu.gatech.cc.jcrasher.writer.JUnitAllImpl;
import edu.gatech.cc.jcrasher.writer.JUnitTestCaseWriter;
import edu.gatech.cc.jcrasher.writer.TestCaseWriter;
import escjava.RefinementSequence;
import escjava.Status;
import escjava.ast.Spec;
import escjava.backpred.FindContributors;

/**
 * Entry point to CnC---Crash 'n Check.
 * 
 * Relies on the following modification of ESC Java 2.08a, which we can
 * include in this jar only in binary form as of the ESC/Java source license.
 * 
 * In escjava.translate.ErrorMsg.print search for the following line,
 * then prepend the next line:
 * if (Info.on || Main.options().pcc) {
 * edu.gatech.cc.cnc.Main.main.jcrasherHook(pruneCC(counterexampleContext).toString(), rd);
 * 
 * In escjava.translate.GetSpec replace the body of getSpecForBody with the following:
 * {
 *   Spec spec = getCommonSpec(rd, scope, premap);
 *   Spec extendedSpec = extendSpecForBody(spec, scope, synTargs);
 *   edu.gatech.cc.cnc.Main.main.storeSpec(extendedSpec);
 *   return extendedSpec;
 * }
 * 
 * You get the ESC/Java1 source of ErrorMsg and all other classes from Compaq:
 * http://research.compaq.com/downloads.html
 * Download all parts of the Java Programming Toolkit Source Release.
 * 
 * Then get the patches to receive ESC/Java2 from:
 * http://sort.ucd.ie/frs/?group_id=97&release_id=27
 * 
 * 2005-08-15 Split jcrasherHook into seven separate methods
 * 
 * @author csallner@gatech.edu (Christoph Csallner)
 */
public class Main extends escjava.Main {
	
	/* Class fields */
	public static boolean IS_DEBUG = false;
	public final static boolean IS_JCRASHER = true;		//run CnC?
	public final static int MAX_ARRAY_LENGTH = 10;  //beyond that no validity checks.
	public final static int MAX_NR_TRIES_PER_COUNTEREXAMPLE = 1000;
	public static int MAX_NR_SOLUTIONS = 3;
	public static int TEST_CASES_PER_SOLUTION = 3;
	public final static int MAX_PLAN_RECURSION = 2; 	//nesting of random search.
	public final static TypeGraph TYPE_SPACE = TypeGraphImpl.instance();
	public static boolean SEARCH_FOR_NPE = false;
	public static boolean SEARCH_FOR_EXCEPTION = false;
	
	public static Main main = null;       						//hack to allow local instance methods.
	//public final static String DEBUG_INPUT = null;	//TODO must be null to parse given file.
  
  /* Exception type expected by ESC/Java */
  public static Class<? extends RuntimeException> expectedException =
    RuntimeException.class;
  public static int expectedLineNumber = 0;         //ignore if smaller than 1.
	
	/* Instance fields */
	protected Spec methSpec = null;										//Static spec from ESC/Java
	protected Map<String,Param> params = null; 				//re-initialized for each counterexample.
	protected Class<?> prevTestee = null;
	protected int prevSeqNrForPrevTestee = 0;  				//numbering starts with 1.
	
	protected static String name = "CnC";	
	protected static String hint =
		"Try `java edu.gatech.cc.cnc.Main -help' for more information."
	;
	
	protected static JUnitAll junitAll = new JUnitAllImpl();  //JUnitAll.java not yet created.

	
	/**
	 * @returns unique number >=1 for next test-class of testee c. 
	 */
	protected int getTestClassSeqNr(Class<?> c) {
		notNull(c);
		if (c != prevTestee) { //reset counter
			prevTestee = c;
			prevSeqNrForPrevTestee = 0;
		}	
		prevSeqNrForPrevTestee += 1;
		return prevSeqNrForPrevTestee;
	}

	
	@Override
	public void preprocess() {
		/* search for all ways to create reachable types--use JCrasher */
    final Set<Class<?>> argsClasses = new LinkedHashSet<Class<?>>();
		for (int i=0; i<loaded.size(); i++) {
			try {
				RefinementSequence rs = ((RefinementSequence) loaded.get(i)); 			
				String fileName = rs.elems.elementAt(0).id.toString();
				if (rs.pkgName != null) {				//default package
					fileName = rs.pkgName.printName() +"." +fileName;
				}
				argsClasses.add(Class.forName(fileName));
			}
			catch(Exception e) {
        e.printStackTrace();
      }			
		}
		TypeGraphImpl.instance().crawl(argsClasses, Visibility.GLOBAL);
		
		super.preprocess();
	}


	/**
	 * Constructor
	 */
	public Main() {
		/* This constructor allows us to create a edu.gatech.cc.jcrasher.testall.escjava.Main
		 * instead of an escjava.Main */
		super();
	}


	/*
	 * return class corresponding to Javafe int constant.
	 */
	protected Class<?> source2class(Type type) {
		switch (type.getTag()) {
			case javafe.ast.TagConstants.INTTYPE : return Integer.TYPE; 
			case javafe.ast.TagConstants.BOOLEANTYPE : return Boolean.TYPE; 
			case javafe.ast.TagConstants.BYTETYPE : return Byte.TYPE; 
			case javafe.ast.TagConstants.SHORTTYPE : return Short.TYPE; 
			case javafe.ast.TagConstants.CHARTYPE : return Character.TYPE; 
			case javafe.ast.TagConstants.LONGTYPE : return Long.TYPE; 
			case javafe.ast.TagConstants.FLOATTYPE : return Float.TYPE; 
			case javafe.ast.TagConstants.DOUBLETYPE : return Double.TYPE; 
			case javafe.ast.TagConstants.ARRAYTYPE :
				return Array.newInstance(source2class(((ArrayType) type).elemType), 0).getClass();				
			default : //non-array reference types
				Class<?> res = null;
				try {
					res = Class.forName(((TypeSig) type.getDecorations()[3]).getExternalName());
				}
				catch (Exception e) {e.printStackTrace();}
				return res;
		}		
	}


	/* 
	 * Return parameter classes 
	 */
	protected Class<?>[] getParamTypes(RoutineDecl rd) {
		Class<?>[] res = new Class[rd.args.size()];
		for (int i = 0; i < res.length; i++) {
			res[i] = source2class(rd.args.elementAt(i).type);
		}
		return res;
	}
	
	
	/*
	 * Return enclosing type
	 */
	protected Class<?> getType(RoutineDecl rd) {
		Class<?> c = null;		
		try { //TODO is TypeSig always stored like this?
			TypeSig typeSig = (TypeSig) rd.parent.getDecorations()[3]; 
			c = Class.forName(typeSig.getExternalName());
		} catch(Exception e) {e.printStackTrace();}
		assert c!=null;
		return c;
	}


	/*
	 * @returns identifier used to store param in the params hashtable
	 */
	protected String getIdColonLoc(GenericVarDecl varDecl, String escOutput) {
		String location = varDecl.id.toString();
		int file = Location.toStreamId(varDecl.locId);
		int line = Location.toLineNumber(varDecl.locId);
		int col = Location.toColumn(varDecl.locId);
		
		String nameLineCol = location+":" +line+"." +col;
		String nameFileLineCol = location+":" +file+"." +line+"." +col;
		
//		if (escOutput.indexOf(nameLineCol)>=0 && escOutput.indexOf(nameFileLineCol)>=0) {
//			throw new IllegalStateException("Found " +nameLineCol +" and " +nameFileLineCol +" in same counterexample.");
//		}
		
		if (escOutput.indexOf(nameFileLineCol)>=0) {	//more descriptive
			return nameFileLineCol;
		}
		if (escOutput.indexOf(nameLineCol)>=0) {
			return nameLineCol;
		}		
		/* neither found in ESC output, default.
		 * Does not matter as no constraints in output anyway. */
		return nameFileLineCol;
	}


	
	
	
	/**
	 * Create a test cases for given solution. 
	 */
	protected Block<?> compileSolution(
      RoutineDecl rd,
      Class<?> testeeType,
      Member m,
      String escOutput)
  {
		Param.resetNames(m, testeeType);       //reset block and i.e. its local names.
		ParamRefType.generateSolution();       //reset cached plans.
		Block<?> block = Param.getBlock();     //will reference paramPlans
		BlockStatement<?>[] paramPlans = new BlockStatement[rd.args.size()]; //one plan per formal param
		
		/* Plan for each parameter */
		for (int i = 0; i < paramPlans.length; i++) {
			Param<?> curWrapper = 
				params.get(getIdColonLoc(rd.args.elementAt(i), escOutput));
			paramPlans[i] = curWrapper.getPlan();
		}
		
		if (m instanceof Constructor) {//constructor
			List<BlockStatement> l = (new ConstructorCallingBlockStatementSequence(
          testeeType, paramPlans, block, (Constructor)m)).getBlockStmts(); 
			block.setBlockStmts(l);
			return block;
		}
		
		check(m instanceof Method);  //method
		if (Modifiers.isStatic(rd.modifiers)) {
      BlockStatementSequence blockStatementSequence =
        new MethodCallingBlockStatementSequence(
            testeeType, paramPlans, block, (Method)m);        
			List<BlockStatement> l = blockStatementSequence.getBlockStmts(); 
			block.setBlockStmts(l);
		}
		else {
			Param instance = params.get("this");
			assert instance!=null;
      JavaCode instancePlan = (JavaCode) instance.getPlan();  //plan for receiver
      
      //FIXME: Following cast is horrible and indicates a design-bug.
      BlockStatementSequence blockStatementSequence;
      blockStatementSequence = new MethodCallingBlockStatementSequence(
          testeeType, paramPlans, block, (Method)m, instancePlan);
        
			List<BlockStatement> l = blockStatementSequence.getBlockStmts(); 
			block.setBlockStmts(l);
		}
		return block;
	}
	
	/* handle RuntimeException thrown by POOC.
	 * TODO this is a bug in POOC, right? */
	protected boolean hasNextIntSolution() {
		boolean res = false;
		try {
			res = ParamInt.generateSolution();
		}
		catch (Exception e) {
			System.out.println("POOC exception: " +e.getMessage());
		}
		return res;
	}
	
	/*
	 * Write test cases to file system, using traditional JCrasher.
	 * @param c testee
	 */
	protected <T> void writeTestCases(RoutineDecl rd, Class<T> c, Member m, String escOutput){
		List<Block> blockList = new Vector<Block>();    //one block per test-case.
		int tries=0; 												//#evaluated solutions.
		int cnt=1;  												//#accepted solutions.
			
		
		while (hasNextIntSolution() && 
			cnt<=edu.gatech.cc.cnc.Main.MAX_NR_SOLUTIONS &&
			tries<=edu.gatech.cc.cnc.Main.MAX_NR_TRIES_PER_COUNTEREXAMPLE)
		{
			tries+=1;
			
			/* generate solution only if array constraint (i=j --> a[i]=a[j]) holds. */
			if (ParamArray.areArraysFunctional()) {
				cnt++;
				
				/* Create three blocks based on same int solution -- hope for JCrasher randomnes */
				for (int i=0; i<TEST_CASES_PER_SOLUTION; i++) {
					blockList.add(compileSolution(rd, c, m, escOutput));
				}				
			}
		}
		Block<?>[] blocks = blockList.toArray(new Block[blockList.size()]);
		int testClassSeqNr = getTestClassSeqNr(c);
		//codeWriter.generateTestFile(c, testClassSeqNr, blocks);
		//codeWriter.generateSuite(c, testClassSeqNr);  //TODO avoid overriding
		boolean doFilter = true;
		TestCaseWriter codeWriter = new JUnitTestCaseWriter<T>(
        c,
        "My comment",
        doFilter,
        blocks,
        testClassSeqNr,
        expectedException,
        expectedLineNumber);
		codeWriter.write();
		
		/* append test suite to JUnitAll */
    junitAll.addTestSuite(c.getName()+"Test"+testClassSeqNr);
	}

	
	
	/**
	 * To be called from escjava.translate.GetSpec.getSpecForBody(..)
	 * for each processed method.
	 * @param extendedSpec contains the result of ExtendedSpecForBody
	 * as defined in ESCJ 16, chapter 7.4 (ESC/Java 1 docs).
	 */
	public void storeSpec(Spec extendedSpec) {
		methSpec = extendedSpec;
	}
	
	

	/**
	 * To be called from escjava.translate.ErrorMsg.print(..)
	 * for each ESC warning.
	 */
	public void jcrasherHook(String escOutput, RoutineDecl rd) {
		if (!edu.gatech.cc.cnc.Main.IS_JCRASHER) {	//no CnC processing
			return;
		}	
		
		params = new Hashtable<String,Param>();           //reset for current counterexample.
		ParamRefType.resetEq();             //reset equivalence relation on reference types.
		ParamIntegral.resetSolver();
		
		processESCwarning(escOutput, rd);
	}
	
	
	/* 
	 * Represent each field by a wrapper
	 */
	protected void addFields(ParseFct fct, RoutineDecl rd, String escOutput, Class<?> testeeType) {
		for (int i=0; i<rd.parent.elems.size(); i++) {
			if (rd.parent.elems.elementAt(i) instanceof FieldDecl) {
				FieldDecl fieldDecl = (FieldDecl) rd.parent.elems.elementAt(i);
				String location = getIdColonLoc(fieldDecl, escOutput);  //id:12.34
				Class<?> type = null;
				try {
					type = testeeType.getDeclaredField(ParseFct.stripEscPostfix(location)).getType();
				}
				catch (NoSuchFieldException e) {
				  /* swallow */
        }
				notNull(type);
        
				Param param = fct.createParam(type, location);
				if (Modifiers.isStatic(fieldDecl.modifiers)) {  //static field
					fct.addParam(location, param);  //could get replaced by method-param.
					/* TODO do we need to model shadowing? */
				}
				else {  //instance field
					if(Modifiers.isStatic(rd.modifiers)==false) {  //only instance method can access.
						ParamComplex thisParam = (ParamComplex) params.get("this");
						thisParam.addElem(location, param);
					}
				} 
			}
		}			
	}
	
	
	
	/**
	 * One parse pass 
	 */
	protected void parse(lr_parser p) {
		try {
			p.parse();
		}
		catch(Exception e) {
			System.out.println(
					"Parse error in constraint " + ParseFct.getCnt() +"\n" +
					"Ignoring remaining constraints");
      e.printStackTrace();
			//if (options().counterexample)
				//e.printStackTrace(System.out);
		}		
	}
	
	
	/**
	 * Parse constraint system produced by ESC:
	 * Add each parsed constraints to params
	 */
	protected void parseESCconstraints(String escOutput) {
//		if (DEBUG_INPUT != null) {
//			parse(new edu.gatech.cc.cnc.firstpass.parser(DEBUG_INPUT, params));
//		}
		
		parse(new edu.gatech.cc.cnc.firstpass.parser(escOutput, params));
		parse(new parser(escOutput, params));
	}

	
	/*
	 * Solve constraints found for complex types
	 */
	protected void solveComplex() {
		List<ParamComplex<?>> complexList = new Vector<ParamComplex<?>>(); //in meth sig.
		
		for (Param<?> param: params.values()) {
			if (param instanceof ParamComplex) {
				complexList.add((ParamComplex<?>) param);
			}
			//FIXME we miss fields of params, right?
		}
		ParamComplex.prepareSolution(complexList);

		//FIXME revise:
		/* Fine-tune distribution of test cases between int-solver and JCrasher */
		MAX_NR_SOLUTIONS = 3;
		TEST_CASES_PER_SOLUTION = 3;			
		for (ParamComplex<?> complex: complexList) {
			if (JCrasherPlanner.instance().hasDefault(complex.getType())) {
				MAX_NR_SOLUTIONS = 2;
				TEST_CASES_PER_SOLUTION = 5;					
			}
		}		
	}
	
	
	protected void solveInt(ParseFct fct) {
		List<ParamIntegral> intList = new Vector<ParamIntegral>(); //for int solver.
		fct.addParamIntegrals(params.values(), intList);
		
		/* Search each ParamRefType for ParamInt fields */
		for (ParamRefType p: ParamRefType.getEq().getKeys()) {
			if (p instanceof ParamArray) {
				intList.add(((ParamArray) p).getArrayLength());  //array length is an int.
			}
			fct.addParamIntegrals(p.getElemKeys(), intList);  //var-indexes of array.
			fct.addParamIntegrals(p.getElemValues(), intList); //int-fields
		}
		ParamIntegral[] intVariables = intList.toArray(new ParamIntegral[intList.size()]);		
		ParamIntegral.prepareSolution(intVariables);		
	}
	

	/* Generate test cases that correspond to ESC's counter-example. */
	protected void generateTests(RoutineDecl rd, String escOutput, Class c, Class[] paramTypes) {
		junitAll.create(c);  //Create JUnitAll
		Method m = null;			
		Constructor con = null;
	
		if (rd instanceof ConstructorDecl) {
			try {
				con = c.getDeclaredConstructor(paramTypes);
				writeTestCases(rd, c, con, escOutput);
			}
			catch(Exception e) {e.printStackTrace();}
		}
		else {
			try {
				m = c.getDeclaredMethod(rd.id().toString(), paramTypes);
				writeTestCases(rd, c, m, escOutput);
			}
			catch(Exception e) {e.printStackTrace();}
		}	
	}
	
	
	
	/* 
	 * From pruned counter-example context
	 * + Determine the method-parameters.  
	 * + Create corresponding constraint objects, where we will 
	 *   aggregate the constraints on this param returned from Simplify.
	 * + Store constraint objects in a map: paraName -> constraint object.
	 *   For example, a -> new ParamInt(formalPara).
	 */	
	protected void processESCwarning(String escOutput, RoutineDecl rd) {				
		ParseFct fct = new ParseFct2(params);
    			
		/* Bridge source-based ESC to bytecode-based JCrasher---load
		 * classes of function parameters.
		 * This assumes that the testee's code is also represented as bytecode
		 * and is reachable for the classloader. */
		Class<?>[] paramTypes = getParamTypes(rd);		
		Class<?> testeeType = getType(rd);	    
		
		/* Add this to params iff instance method. */
		if (Modifiers.isStatic(rd.modifiers) == false) {
			Param<?> thisParam = fct.createParam(testeeType, "this");
			fct.addParam("this", thisParam);
		}
			
		/* Represent each field by a wrapper */
		addFields(fct, rd, escOutput, testeeType);			
			
		/* Represent each formal parameter by a wrapper. */
		for (int i=0; i<paramTypes.length; i++) {  //list of formal params, excluding this.
			String location = getIdColonLoc(rd.args.elementAt(i), escOutput); 
			Param<?> param = fct.createParam(paramTypes[i], location);
			fct.addParam(location, param);  //id:12.34
		}
		
		/* Parse ESC's counter-example---add constraints to params. */
		parseESCconstraints(escOutput); 
		
		/* Collect complex params from params list.
		 * Propagate identity from object (o1==o2) to object-fields (o1.f==o2.f). 
		 * Fine-tune distribution of test cases between int-solver and JCrasher */
		solveComplex();				
					
		/* Search for ParamInt params and solve their constraints. */
		solveInt(fct);
		
		//Out.debug(getInternalMappings(c));
				
		/* Generate test cases that correspond to ESC's counter-example. */
		generateTests(rd, escOutput, testeeType, paramTypes);
    
    /* Reset to default */
    expectedException = RuntimeException.class;
    expectedLineNumber = 0;
	}
	
	
	/*
	 * Print debug info
	 */
	protected String getInternalMappings(Class c) {
		/* Get info on ESC mapping stream --> source file */
		StringBuffer s = new StringBuffer(c.getCanonicalName()+"\n====================");
		List fileNames = LocationManagerCorrelatedReader.fileNumbersToNames();
		for (int i=0; i<fileNames.size(); i++) {
			s.append(fileNames.get(i));
		}
		s.append("====================\n");
		
		/* Variable names */
		s.append(params.toString());
		return s.toString();
	}

	
	private boolean isConstructorOfAbstractClass(RoutineDecl r) {
		if (r instanceof ConstructorDecl &&
				Modifiers.isAbstract(r.parent.getModifiers())) {
			return true;
		}
		else {return false;}		
	}
	
	/**
	 * Run our analyses only on public methods of public top-level classes.
   * TODO: ESC/Java also analyzes methods declared by nested classes.
   * This should be easy for us to support, but JCrasher does not currently
   * do it so the results would be harder to compare.
	 */
  public int doProving(Expr vc, RoutineDecl r, javafe.util.Set directTargets,
			FindContributors scope) {
		if (Modifiers.isPublic(r.modifiers)           //public method.
			//&& !Modifiers.isPrivate(r.parent.getModifiers()) //not declared by private class.
      && (r.parent.parent==null)                  //declared by top-level class.  
			&& isConstructorOfAbstractClass(r)==false)  //not a constructor of abstract class.
		{
			return super.doProving(vc, r, directTargets, scope);
		}
		else {  //non-public defaults to ok.
			return Status.STATICCHECKED_OK;
		}
  }
  

	/**
	 * Ensure that this.Main() is called instead of super.Main().
	 */
	public static int compile(String[] args) {
		int res;
		
		main = new Main();
		res = main.run(args);
		junitAll.finish();		//created in jcrasherHook (nop else)
		return res;
	}


	protected static void setCygwinEnv() {	
		/* Simplify.Simplify reads the system propery "simplify" as
		 * java.lang.System.getProperty("simplify", "/usr/local/escjava/bin/Simplify"). */
		//FIXME why does Eclipse need the following line and can't read
		//the simplify environment variable?
		//pass -simplify Simplify-1.5.4.exe as argument to CnC.
		//java.lang.System.setProperty("simplify", "Simplify-1.5.4.exe");
	}


	/**
	 * Start up an instance of this tool, pass args.
	 *
	 * Main entry point---delegates almost everything to super.
	 */
	//@ requires \nonnullelements(args)
	public static void main(String[] args) {
		//setCygwinEnv();
    
    JCrasher jcrasher = new JCrasher();
		jcrasher.setNameAndHint(name, hint);

		/* we interpret first arguments only. */
		int foundArgs = 1;		
		while (args.length>0 && foundArgs>0) {  //TODO move to gnu.getopt.
			foundArgs = 0; //processed zero arguments so far.
			
			if (args[0].equals("-debug")) {
				IS_DEBUG = true;
				foundArgs = 1;
			}			
			if (args[0].equals("-NPE")) {
				SEARCH_FOR_NPE = true;
				foundArgs = 1;
			}
			if (args[0].equals("-explicitException")) {
				SEARCH_FOR_EXCEPTION = true;
				foundArgs = 1;
			}			
			if (args[0].equals("-outdir")) {
				jcrasher.parseOutDir(args[1]);
				foundArgs = 2;
			}						
			if (foundArgs>0) {  //remove processed args from list.
				String[] allArgs = args;
				args = new String[allArgs.length-foundArgs];
				System.arraycopy(allArgs, foundArgs, args, 0, args.length);				
			}
		}
		/* Removed our arguments from args. */
		
		
		
		/* Add -nowarn switches. Only warn of the following six cases:
		 * + ArrayStore ``A[I] = E when the value of E is not assignment compatible with the actual element type of A.''
		 * + Cast ``(T)E when the value of E cannot be cast to the type E.''
		 * + ``array access A[I] when the value of the index I is negative.''
		 * + ``array access A[I] when A.length <= I.''
		 * + ``allocate an array of negative length.''
		 * + integer division by zero. */
		List<String> argList = new Vector<String>();
		argList.addAll(Arrays.asList(
				"-nowarn", "All",
				"-warn", "ArrayStore",
				"-warn", "Cast",
				"-warn", "IndexNegative",
				"-warn", "IndexTooBig",
				"-warn", "NegSize",
				"-warn", "ZeroDiv"));
		if (SEARCH_FOR_EXCEPTION) {
			argList.addAll(Arrays.asList(
					"-warn", "Exception"));
		}		
		if (SEARCH_FOR_NPE) {
			argList.addAll(Arrays.asList(
					"-warn", "Null"));
		}
		argList.addAll(Arrays.asList(args));
		
//		String[] nowarnAndArgs = null;
//		int defaultArgs = 16;
//		int optArgs = 2;
//		if (SEARCH_FOR_NPE) {nowarnAndArgs = new String[defaultArgs+optArgs+args.length];}
//		else {nowarnAndArgs = new String[defaultArgs+args.length];}
//		nowarnAndArgs[0] = "-nowarn";				//1
//		nowarnAndArgs[1] = "All";						//...
//		nowarnAndArgs[2] = "-warn";
//		nowarnAndArgs[3] = "ArrayStore";
//		nowarnAndArgs[4] = "-warn";
//		nowarnAndArgs[5] = "Cast";
//		nowarnAndArgs[6] = "-warn";
//		nowarnAndArgs[7] = "IndexNegative";
//		nowarnAndArgs[8] = "-warn";
//		nowarnAndArgs[9] = "IndexTooBig";
//		nowarnAndArgs[10] = "-warn";
//		nowarnAndArgs[11] = "NegSize";
//		nowarnAndArgs[12] = "-warn";
//		nowarnAndArgs[13] = "ZeroDiv";			//14
//		nowarnAndArgs[14] = "-warn";				
//		nowarnAndArgs[15] = "Exception";		//16
//				
//		/*
//		nowarnAndArgs[16] = "-warn";				//Warn that Daikon-inferred invariant violated
//		nowarnAndArgs[17] = "Invariant";		//16
//		*/
//		if (SEARCH_FOR_NPE) {								//optArgs:
//			nowarnAndArgs[defaultArgs] = "-warn";			//1
//			nowarnAndArgs[defaultArgs+1] = "Null";		//2
//			System.arraycopy(args, 0, nowarnAndArgs, defaultArgs+optArgs, args.length);
//		}
//		else {
//			System.arraycopy(args, 0, nowarnAndArgs, defaultArgs, args.length);
//		}
		

		/* real work */
		long startTime= System.currentTimeMillis(); //run time measurement
		//compile(nowarnAndArgs);			//main processing
		compile(argList.toArray(new String[argList.size()]));			//main processing
		//int exitcode = compile(nowarnAndArgs);
		long endTime= System.currentTimeMillis();  	//run time measurement
		System.out.println("runtime = " +Long.toString((endTime-startTime)/1000) +" seconds.");
	}
}
